Our type discipline builds upon the one given in~\cite{DBLP:journals/entcs/YoshidaV07},
extending it so as to account for disciplined runtime adaptation.
%\cite{DBLP:conf/ppdp/GarraldaCD06}.
%As mentioned in the Introduction, a 
A
main criteria in the design of our type discipline is \emph{conservativity}:
we would like to enforce both disciplined communication and disciplined adaptation by preserving as much as possible standard models of session types.
Thus, our type syntax (given below) is rather standard; also, we rely on a typing judgment which extends usual notions with an  \emph{interface}~$\INT$. Intuitively, interfaces describe the services declared in a given process.
%Our type syntax is as follows: %defined next, contains the usual session types constructs: %---we exclude recursive types.

%As such, the type syntax is divided into three categories: \emph{basic types}, which  handle expressions; 
%\emph{pre-session types} describing a channel's ability for sending/receiving messages and offering/selecting be\-hav\-iors; 
%\emph{session types} representing well-formed session-typed be\-hav\-ior. %; and
%\emph{channel types}, which can be a session type or a \emph{used session}~$\bot$. %this will be made clear later on).

%We extend the judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06} with an \emph{interface} $\INT$---the collection of all session types declared in a given process. 
%
%Formally, we have:

%\end{document}
 
\begin{definition}[Types]\label{d:types}
The syntax of 
 \emph{basic types} (ranged over $\capab, \sigma,   \ldots$) %, \emph{pre-session types} ($\zeta$), 
 and
 %(qualified) 
 \emph{session types} (ranged over $\ST, \beta, \ldots$)
% and \emph{channel types} ($\omega$) 
is given in Table~\ref{tab:types}.
\end{definition}

\begin{table}[t]
\textsc{Types}
$$
\begin{array}{lclr}
\capab, \sigma & ::= & \mathsf{int} \sepr \mathsf{bool} \sepr \dots ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\tilde{\capab}).\alpha \sepr ?(\tilde{\capab}).\alpha & \text{send, receive} \\ 
		& \sepr &  !(\beta).\alpha \sepr ?(\beta).\alpha & \text{throw, catch} \\ 
		& \sepr &  \&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}  \quad &  \text{branch} \\
		& \sepr &  \oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}  &  \text{select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session}
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\INT &::= &  \emptyset \sepr \INT, \langle a: \ST, h \rangle & \text{interface} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  [k:\ST]  & \text{typing with active sessions}\\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST_\qua} \rangle \quad& \text{first-order environment}\\
\Theta &::= &  \emptyset \sepr  \Theta,\mathsf{X}:\INT \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
$$  
\caption{Types and Typing Environments}\label{tab:types}
\end{table}



% We use $t, t', \ldots$ to range over \emph{type variables}; also, we 
% require recursive types to be \emph{contractive}, i.e., not 
% containing a subexpression of the form $\mu t.\mu t_1.\cdots.\mu t_n.t$.
% Binder $\mu$ gives rises to standard notions of free/bound type variables; 
% $\mathsf{ftv}(\zeta)$ denotes the free type variables in $\zeta$.
% We consider session types modulo folding/unfolding of recursive types.
%\todo{contractive types?}
We recall the intuitive meaning of session types. 
Type $?(\tilde{\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives values of types $\tilde{\capab}$ (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards.
In a complementary way, type $!(\tilde{\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends values (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}$ describes a branching behavior, or external choice, along a channel:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$. This is an internal choice, which continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior. 
We now introduce the central notion of  \emph{duality} for (session) types.


\begin{definition}[Duality]\label{d:dual}
Given a session type $\ST$, 
its \emph{dual}
(noted $\overline{\ST}$) is inductively defined in Table~\ref{tab:dual}.
\begin{table}[t]
$$
\begin{array}{rcl}
 \overline{\epsilon} & =  & \epsilon\\
 \overline{!(\tilde{\capab}).\ST} & =  & ?(\tilde{\capab}).\overline{\ST} \\
 \overline{?(\tilde{\capab}).\ST} & =  & !(\tilde{\capab}).\overline{\ST} \\
 \overline{!(\beta).\ST} & =  & ?(\beta).\overline{\ST} \\
 \overline{?(\beta).\ST} & =  & !(\beta).\overline{\ST} \\
% \overline{t} &\!\!=\! & t \\
 %\overline{\mu t.\ST} &\!\!=\! & \mu t.\overline{\ST}\\
 \overline{\&\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\! & \oplus\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}\\
 \overline{ \oplus\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\!& \&\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}
\end{array}
$$ %\vspace{-4mm}
\caption{Dual of session types}\label{tab:dual}
\end{table}
\end{definition}

Before introducing our notions of typing environments, we formally define the concept of interface, motivated above.

\begin{definition}[Interfaces]\label{d:interf}
An \emph{interface} $\INT$ is a set of pairs  $\langle a: \ST, h\rangle$ where 
$a$ is name, $\ST$ is a session type, and either $h> 0$ or $h = \infty$.
The extension of an interface $\INT$ with a pair $\langle a: \ST, h\rangle$, written $\INT \addelta \inter{a}{\alpha}{h}$,
is defined as follows:
$$
\INT \addelta \inter{a}{\alpha}{h} \triangleq
\begin{cases}
\INT' \cup \{\inter{a}{\ST}{h + j} \} & \text{if } \exists\INT'. \,  \INT = \INT' \cup \{\inter{a}{\ST}{j} \}	\\
\INT \cup \{\inter{a}{\ST}{h}\} & \text{otherwise} 
\end{cases}
$$
Given $\INT$, we write $\INT_\quau$ 
and $\INT_\qual$
to denote sets $\{ \inter{a}{\ST}{h} \,|\, \inter{a}{\ST}{h} \in \INT \land h = \infty\}$ and
$\INT - \INT_\quau$, respectively. \\
Moreover, we write $\INT \unres$ 
to denote the set $\{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT_\qual \} \cup \INT_\quau$.
%Finally we define the  function $$\unres(\INT) \triangleq \{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT \}$$
\end{definition}


We recall that $\infty + 1 = \infty$.
Intuitively, interfaces capture the services declared in a process (i.e., an assignment from names to session types)
together with
the number of times such a service is declared ($j>0$ if a type is linear; $\infty$ otherwise).
In $\INT$, services are recorded at most once; several occurrences of the same linear service are captured
by the second component of the pair.   
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\inter{a}{\ST}{1} \}$ and 
$\INT \addelta \{\inter{a}{\ST}{\infty} \}$, respectively.
The extension of $\addelta$ from single pairs $\inter{a}{\ST}{h}$ 
to interfaces, denoted $\INT_1 \addelta \INT_2$, is as expected. 

It is useful to relate different interfaces. % which only differ in the linear services they contain.
This is the intention of the 
relation $\intpr$ over interfaces, defined next.

\begin{definition}[Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\INT_\quau \subseteq \INT'_\quau$.
\item $\forall \inter{a}{\alpha}{h} \in \INT_\qual $  then 
$ \inter{a}{\alpha}{h'} \in \INT'_\qual $, for some $h'$ such that $h \leq h'$
\end{enumerate}
\end{definition}

\begin{lemma}
Relation \intpr is a preorder.
\end{lemma}

As we will see, our typing system will be parametric on the definition of \intpr.
Alternative definitions for this relation are discussed in Sect.~\ref{sec:int}.

The typing environments we rely on are defined in the lower part of Table~\ref{tab:types}.
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$.
As typical in session types disciplines, 
typing $\ActS$ collects 
assignments from channels to session types, therefore describing 
currently active sessions. 
Unlike usual disciplines, however, in $\ActS$ we also include \emph{bracketed assignments}, denoted $[\kappa^p:\ST]$,
which represent active but restricted sessions. 
As we discuss below, bracketed assignments arise in the typing of channel restriction, 
and are key to keep a precise count of the active sessions in a given location. 
We write $dom(\ActS)$ to denote the set $\{ \cha^p \mid \cha^p:\ST \in \ActS \lor [\cha^p:\ST] \in \ActS\}$.
$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
Within the interface, session types can be linear ($\qual$) or unrestricted ($\quau$). 
While $\qual$ is used for those session types to be used just once, 
$\quau$ qualifies those session types intended to feature a persistent behavior.
The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments is relevant to update processes, the latter concern located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
%\jp{The following is a bit strange for locations are also in $\T$; I would write $vdom(\T)$ if you only care about variables.} \todo{
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
%}
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$. We then have:

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.


\begin{table}[th!]
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:Exp}]{\Gamma \vdash e:\capab}{} \ \
\infer[\rulename{t:NVar}]{\Gamma, x:\capab \vdash x:\capab}{} \ \ 
\infer[\rulename{t:Nil}]{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}{}
\\ \\
 \infer[\rulename{t:LocEnv}]{\Theta, l:\INT \vdash l:\INT}{} \quad
\infer[\rulename{t:PVar}]{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}{}
\\
\\
 \infer[\rulename{t:Accept}]{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}}{
\Gamma \vdash a: \langle \ST_\qual , \overline{\ST_\qual } \rangle \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}} 
} 
\\
\\
 \infer[\rulename{t:RepAccept}]{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}}
 {
\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
}
\\
\\
 \infer[\rulename{t:Request}]{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST_\qual }}}} 
 {
\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qual} \rangle \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
}
\\
\\
 \infer[\rulename{t:Clo}]{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }
 \\ \\
 \infer[\rulename{t:Loc} ]{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}}
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
 }
 \\
\\
 \infer[\rulename{t:Adapt} ]{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} 
{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}
\\
 \\
 \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}
 \\
\\
 \infer[\rulename{t:Par}]{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }
 \end{array}
 $$
\caption{Well-typed processes (I)} \label{tab:ts}
\end{table}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{table}[!t]
%$$
%\begin{array}{cr}
%\cfrac{}{\Gamma \vdash e:\capab} \qquad 
%\cfrac{}{\Gamma, x:\capab \vdash x:\capab}  \qquad
%\cfrac{}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}} 
% & \rulename{t:Exp},  \rulename{t:NVar}, \rulename{t:Nil} \\
%
%\cfrac{}{\Theta, l:\INT \vdash l:\INT}
%\quad \cfrac{}{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}
%&    \rulename{t:LocEnv},  \rulename{t:PVar}   \vspace{2mm}\\
%
% \cfrac{
%\Gamma \vdash a: \langle \ST_\qual , \overline{\ST_\qual } \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}} 
%& 
%\rulename{t:Accept} \vspace{2mm} 
%\\
%
% \cfrac{
%\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}} 
%& 
%\rulename{t:RepAccept} \vspace{2mm} 
%\\
%
%% \cfrac{
%%\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \quad
%%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\todo{$\INT_\quau$}}} 
%%}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT_\quau \addelta \, a: \ST_\quau}}} 
%%& 
%%\rulename{t:RepAcceptProp} \vspace{2mm} 
%%\\
%
%\cfrac{
%\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qual} \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST_\qual }}}} 
%& 
%\rulename{t:Request} \vspace{2mm} 
%\\
% \cfrac{\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}} & \rulename{t:Clo} \vspace{2mm} \\
%
%\cfrac{
%       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
% }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}} &  \rulename{t:Loc}  \vspace{2mm}
%\\
%
%
%\cfrac{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} & \rulename{t:Adapt}  \vspace{2mm}
%
%\\
% 
%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}} 
%& \rulename{t:CRes} 
%\vspace{2mm}
%
%\\
%\cfrac{
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
% \qquad
% \INT = \INT_1 \addelta \INT_2}{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT}}} & \rulename{t:Par}  
%\end{array}
%$$
%\caption{Well-typed processes (I)} \label{tab:ts}
%\end{table}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{table}[th!]
$$
\begin{array}{c}
\infer[\rulename{t:Thr}]{\judgebis{\env{\Gamma}{\Theta}}{\throw{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}} 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}
\\  
\\
\infer[\rulename{t:Cat}]{\judgebis{\env{\Gamma}{\Theta}}{\catch{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}
\\
\\
\infer[\rulename{t:In}]{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{\tilde{x}}.P }{\type{\ActS, k:?(\tilde{\capab}).\ST}{ \INT}}}
{\judgebis{\env{\Gamma, \tilde{x}:\tilde{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}
\\
\\
\infer[\rulename{t:Out}]{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{\tilde{e}}.P}{\type{\ActS, k:!(\tilde{\capab}).\ST}{ \INT}}}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \Gamma \vdash \tilde{e}:\tilde{\capab}}
\\
\\
\infer[\rulename{t:Weak}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}} 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \qquad \cha^+, \cha^- \notin dom(\ActS)}
\\
\\ 
\infer[\rulename{t:If}]{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
 {
 \Gamma \vdash e:\mathsf{bool} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }
 \\
  \\
\infer[\rulename{t:Bra}]{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \! \parallel \!\cdots \!\parallel n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_k{:}\ST_m \}}{\INT}}} 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT}} 
\ 
\cdots
\
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT}} %\qquad \rulename{t:Bra}
 }
 \\
\\
\infer[\rulename{t:Sel}]{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
} 
\end{array}
$$% \vspace{-4mm}
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}




We comment on some non standard rules in Table~\ref{tab:ts}.
Given a process which implements session type $\ST$  on channel $x$, 
rule \rulename{t:Accept} types linear service acceptance processes on name $a$. 
Observe how $x$ is removed from $\ActS$ whereas
 $\INT$ is appropriately extended with $a : \ST_\qual$. Rule \rulename{t:RepAccept} is its analogous in an unrestricted setting.
In that rule, observe how the linear services in  $\INT$ are ``promoted'' to unrestricted services via $\INT\unres$ (cf. Def.~\ref{d:interf}).
%\todo{
Linear services that appear in the context of a persistent service $a$ are meant to be executed exactly once for each copy of $a$. 
In fact, after promotion the declaration in $\Gamma$ for a linear service $b:\langle \ST_{\qual}, \overline{\ST_{\qual}} \rangle$ remains unchanged, but its entry in $\INT$ should be $\inter{b}{\ST}{\infty}$, as we could now observe an unbounded number of linear executions of $b$.
%}
%\jp{Cinzia, please check I didn't modified the intended meaning of your text.}
Given these typing rules, rule \rulename{t:Request} should be self-explanatory.
Rule \rulename{t:CRes} types channel restriction. 
The main difference wrt usual typing rules for channel restriction (cf.~\cite{DBLP:journals/entcs/YoshidaV07}) is that 
restricted end-points are not removed from $\ActS$ but kept in bracketed form. 
This allows us to use typing $\ActS$ to have an exact count of open, possibly restricted, sessions in a process.
Rule \rulename{t:Close} types the explicit session closure construct, extending 
$\ActS$ with a fresh channel which is assigned to an empty session type. 
This may be useful to understand why our typing rule for the inactive process (rule \rulename{t:Nil})
requires an empty typing $\Delta$.
%\jp{Far notare la nostra regola Rule \rulename{t:Nil} inizia da un $\Delta$ vuoto...}
Rule \rulename{t:Loc} performs two checks to type located processes. First, the runtime annotation 
$h$ is computed by counting the assignments (standard and bracketed) declared in $\ActS$.
Second, the rule checks that the interface of the located process is less  or equal (in the sense of $\intpr$, cf. Def.~\ref{d:intpre}) than the
declared interface of the given location. 
Informally, this ensures that the process behavior does not ``exceed'' the expected behavior within the location.
It is worth observing how a typed located processes has the exact same typing and interface of its contained process:
this is how transparency of locations arises in typing.
Finally, rule \rulename{t:Adapt} types update processes. Observe how the interface associated to the process variable of the given 
 adaptation routine should match with the declared interfaces for the given location. 
However, for simplicity we establish no condition on the relation between $\INT$ (the expected interface) 
and $\INT'$ (the interface of the adaptation routine $P(\mathsf{X})$)---Sect.~\ref{sec:int} discusses an alternative formulation.
%\jp{Should we say something about $\INT'$?, yes but not here}
%This way, the rule guarantees that the process resulting from an update action has the declared interfaces. 



%Rule \rulename{t:Par} puts processes in parallel. 
%Rules \rulename{t:PVar}  handle process  variables. 
%Rule \rulename{t:Weak} handles all those processes in which $\restr{c}{P} \equiv P$ holds, and 
%\rulename{t:CRes} types channel restriction. 
%While rules \rulename{t:Cat} and \rulename{t:Thr} handle delegation,
%rules \rulename{t:In}, \rulename{t:Out},  \rulename{t:If}, 
%\rulename{t:Bra},  and \rulename{t:Sel} are standard.




%\todo{Properties of the type system
%\begin{enumerate}
%\item Weakening and strengthening lemmas
%\item Substitution lemma
%\item Subject congruence 
%\item Subject reduction, for balanced environments
%\item Type safety (with appropriate definitions of error)
%\end{enumerate}
%}
